Iof proof for Lemma int entire a:
1. a :
2. b :
3. a
0
4. b
0
5.
((a * b) = 0)
a * b 0
by (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term)
.| 12,41 |
0
0
((a * b) = 0)
a * b 0
by (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term)
.
| Definitions | b  T |